OM: Lambda Assembler

Сегодня откомпилировалась базовая библиотека Морте с помощью Om. Эсктраченый
эрланг код на индуктивных списках вроде работает (то что я постил раньше, фолд
миллиона элементов). Нужно больше тестов. Размер компилятора пока занимает 400
строк кода.

Непрошло и три месяца как Групоид Инфинити, Инк. написала компилятор с
зависимыми типами для Erlang инфраструктуры — как раз к проведению конференции
Erlang Factory. Скоро вы сможете забыть про лямбда куб обычный и с наслаждением
войти в неизведанный Космический Куб — полную чашу Инфиниту Групоидов и
Инфинити Моноидов, и все это на старом добром говне мамонта Эрланге 86 года
выпуска. А также js и других нетипизированных языков, которые нас интересуют в
гораздо меньшей мере.

Ом работает в MLTT сеттинге и реализует модель PTS, где основные параметры —
сорта, аксиомы и правила вывода, задаются с помощью формул, а не с помощью
перечислений, или как еще говорят предикативная модель:

    S = *{n}, n : nat
    A = *{i} : *{i+1}
    R = *{i} -> *{j} : *{max i j}

Детальное описание этих параметров смотрите в Lambda Calculi with Types Хенка
Барендрегта, а также статью Henk: Intermediate Language Саймона Пайтона и Эрика
Мейера. Таким образом, можно говорить о том, что Ом в своей теоритической
основе не хуже чем Agda, Lean, Coq и другие MLTT пруверы. Отличает его только
то, как вы знаете уже по моим прошлым постам, что он внутри все элиминаторы и
кодировщики индуткивных титпов реализует посредством своей макросистемы, а не
как вшитые в ядро тайпчекера типы. Ближе всех из существующих пруверов — это
божественный и самый быстрый в мире CiC прувер Lean. Если вы не пробовали еще
плагин emacs для Lean, быстро пробуйте и сравните с коковским ProofGeneral.
Небо и земля! Мы в Lean тестируем термы и строим метамодель кодировщика --
фибрационные диалгебры и взятие их лимитов.

> 'List':
'(<=<)'/0      '(<|>)'/0      '(=<<)'/0      '(>=>)'/0      '(>>=)'/0
'Cons'/0       'Nil'/0        all/0          any/0          concat/0
empty/0        length/0       map/0          module_info/0  module_info/1
null/0         pure/0         replicate/0    reverse/0

> 'Nat':
'(*)'/0        '(+)'/0        '0'/0          'Succ'/0       'Zero'/0
module_info/0  module_info/1  odd/0          product/0      sum/0

> 'Bool':
'False'/0      'True'/0       'and'/0        'not'/0        'or'/0
module_info/0  module_info/1

> 'Maybe':
'(<=<)'/0      '(<|>)'/0      '(=<<)'/0      '(>=>)'/0      '(>>=)'/0
'0'/0          'Just'/0       'Nothing'/0    empty/0        map/0
module_info/0  module_info/1  pure/0

Напоминаю как пользоваться OM:

$ brew install erlang
$ wget https://github.com/groupoid/om/releases/download/0.3/om
$ chmod +x om
$ ./om


Ом мониторит директорию стандартную директорию для Erlang'а — "priv", в которой
находятся каталоги с разными кодировками Church, Scott, а возможно и с разными
прелюдиями и типами. В поставку Ом входят два закодированных парадокса: Жирара
и Хуркенса, которые Ом должен будет схватить, как только мы пофиксаем все
ошибки.

$ om modes list
["girard","hurkens","hurkens-src","normal","setoids"]

Ом обладает набором комбинаторов, которые вы можете выстраивать в пайп:

$ om help me
[{a,[expr],"to parse. Returns {_,_}=Term or {error,_}."},
 {type,[term],"typechecks and returns Type term."},
 {erase,[term],"to untyped term. Returns {Term,Type}."},
 {file,[name],"load file as binary."},
 {str,[binary],"lexical tokenizer."},
 {parse,[tokens],"parse given tokens into {_,_} term."},
 {fst,[{x,y}],"returns first element of a pair."},
 {snd,[{x,y}],"returns second element of a pair."},
 {debug,[bool],"enable/disable debug output."},
 {mode,[name],"select metaverse folder."},
 {modes,[],"list all metaverses."}]

Покажем на примере:

$ om fst erase a "#List/Cons" , mode normal
ok
{{"λ",{'Head',0}},
 {any,{{"λ",{'Tail',0}},
       {any,{{"λ",{'Cons',0}},
             {any,{{"λ",{'Nil',0}},
                   {any,{app,{{app,{{var,{'Cons',0}},{var,{'Head',0}}}},
                              {app,{{app,{{var,{'Tail',0}},{var,{'Cons',0}}}},
                                    {var,{'Nil',0}}}}}}}}}}}}}}

Сам Ом, будучи консольной утилитой, имеет также встроенный шел (Эрланг шелл).
Просто запустите его без параметров.

$ om
> [ {A,C} || {A,C,_} <- om:all() ].
[{"hurkens","PASSED"},
 {"normal","PASSED"},
 {"setoids","PASSED"},
 {"src-hurkens","PASSED"}]
> om:mode("setoids").
> om:snd(om:erase(om:a("#DEP.AND"))).
{star,1}

Надеюсь вам понравится! Все это стало возможным благодаря ZEIT_RAFFER и
NPONECCOP, которые непокладая сил думают над устройством внутреннего языка
пространства :-)

__________________
[1]. http://groupoid.space/pts/pure
[2]. https://github.com/groupoid/om